Inference at * 
Iof proof for Lemma member-zip:


  A, B:Type, xs:(A List), ys:(B List), x:A, y:B.
  (<x, y>  zip(xs;ys))  {(x  xs) & (y  ys)} 

latex

 by InductionOnList 

latex

 1: 

 1: 1. A : Type
 1: 2. B : Type
 1: 3. A List
 1:   ys:(B List), x:A, y:B. (<x, y>  zip([];ys))  {(x  []) & (y  ys)}
 2: 

 2: 1. A : Type
 2: 2. B : Type
 2: 3. A List
 2: 4. u : A
 2: 5. v : A List
 2: 6. ys:(B List), x:A, y:B. (<x, y>  zip(v;ys))  {(x  v) & (y  ys)}
 2:   ys:(B List), x:A, y:B. (<x, y>  zip([u / v];ys))  {(x  [u / v]) & (y  ys)}
 .

Definitions

Type, x:A. B(x), P  Q, {T}, P & Q, (x  l), x:A  B(x), x:AB(x), type List, t  T